#include "Backtracker.cuh"

__device__ Backtracker::Backtracker(VariablesStateHandler* handler,
			WatchedClausesList * watched_clauses, CUDAListGraph * graph
#ifdef ENABLE_STATISTICS
			,RuntimeStatistics * stats
#endif
		)
{
#ifdef USE_ASSERTIONS
	assert(handler != NULL);
#endif
	this->variables_handler = handler;
	this->watched_clauses = watched_clauses;
	this->graph = graph;
#ifdef ENABLE_STATISTICS
	this->stats = stats;
#endif
}

__device__ void Backtracker::backtrack_to(int decision_level)
{
#ifdef ENABLE_STATISTICS
	stats->signal_backtrack_start(variables_handler->number_of_decisions());
#endif

	variables_handler->backtrack_to(decision_level);

	if(graph != NULL)
	{
		graph->backtrack_to(decision_level);
	}

	if(watched_clauses != NULL)
		watched_clauses->handle_backtrack();
#ifdef ENABLE_STATISTICS
	stats->signal_backtrack_stop(variables_handler->number_of_decisions());
#endif
}

__device__ sat_status Backtracker::handle_backtrack(int decision_level)
{
	return handle_backtrack(decision_level, true);
}


__device__ sat_status Backtracker::handle_backtrack(int decision_level, bool switch_literal)
{

	Decision to_backtrack =
			variables_handler->last_non_branched_decision(decision_level);

	to_backtrack.branched = true;
	to_backtrack.literal = ~to_backtrack.literal;


	//if(decision_level < 0 || variables_handler->get_decision_level() == -1)
	if(to_backtrack.decision_level == NULL_DECISION_LEVEL)
	{
		backtrack_to(0);
		return UNSAT;
	}

	if(switch_literal)
	{
		backtrack_to(to_backtrack.decision_level - 1);
		variables_handler->new_decision(to_backtrack);
		variables_handler->set_decision_level(variables_handler->get_decision_level()+1);
		if(graph != NULL)
		{
			Decision implication = to_backtrack;
			implication.implicated_from_formula = false;
			graph->set(implication);
		}
	}
	else
	{
		if(to_backtrack.decision_level == decision_level)
			backtrack_to(to_backtrack.decision_level - 1);
		else
			backtrack_to(to_backtrack.decision_level);
	}


	return UNDEF;

}

__device__ sat_status Backtracker::handle_chronological_backtrack()
{
	return handle_backtrack(variables_handler->get_decision_level());
}

__device__ void Backtracker::set_watched_clauses(WatchedClausesList * watched_clause)
{
	this->watched_clauses = watched_clause;
}
